| Definitions |  x:A. B(x), P  Q, i <z j,   b, tl(l), i  z j, nth_tl(n;as), hd(l), A B, i j < k, Y, Top, ||as||, {i..j }, l[i], A c B, {T}, SQType(T), MaName, False, Rpre-a(x1), Rpre-ds(x1), Rpre?(x1), Rsends-ds(x1), Rbframe-L(x1), Rbframe-k(x1), Rbframe?(x1), Rsframe-L(x1), Rsends-knd(x1), Rsends-g(x1), Rsframe-tag(x1), Rsends-l(x1), Rsframe-lnk(x1), Rsframe?(x1), Rsends?(x1), Rrframe-L(x1), Reffect-ds(x1), Rrframe-x(x1), Rrframe?(x1), Raframe-L(x1), Raframe-k(x1), Raframe?(x1), Rframe-L(x1), Reffect-knd(x1), Reffect-x(x1), Rframe-x(x1), Rframe?(x1), Reffect?(x1),  , True, if b then t else f fi , tt, ff,   x. t(x), t  T, R-frame-compat(A;B), P & Q, Rnone?(x1), Rplus?(x1),  b, A, P   Q, Realizer,  x:A. B(x), Dec(P), P  Q, P Q, x(s), Unit, R-loc(R), R-names(A), Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), left  right, Rnone(),  , fpf-domain(f) |
| Lemmas | locl wf, member-remove-repeats, remove-repeats wf, member append, append wf, IdLnk sq, rcv wf, ldst wf, member map, decidable equal MaName, cons member, member-fpf-dom, Knd sq, le wf, length wf nat, non neg length, length wf1, top wf, fpf-domain wf, locknd wf, select member, Id sq, LocKnd wf, pi1 wf, map wf, es realizer wf, Rrframe wf, fpf-trivial-subtype-top, id-deq wf, fpf-dom wf, Rbframe wf, Raframe wf, Rpre wf, Rsends wf, Reffect wf, Rsframe wf, Rframe wf, Rnone? wf, R-names wf, l member wf, MaName wf, Rinit wf, R-loc wf, false wf, Rplus? wf, assert wf, true wf, not wf, bool wf, finite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, Id wf, unit wf |